Nuprl Lemma : dcdr-to-bool-equivalence
11,40
postcript
pdf
P
:
,
d
:Dec(
P
). (
[
d
]
)
P
latex
ProofTree
Definitions
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
[
d
]
,
b
,
Dec(
P
)
,
x
:
A
.
B
(
x
)
,
t
T
,
,
Type
,
P
Q
,
left
+
right
,
False
,
True
,
A
Lemmas
decidable
wf
,
dcdr-to-bool
wf
,
assert
wf
origin
P:
, d:Dec(P). (
[d]
) 
P
P:, d:Dec(P). ([d]) P
Q Q Qbx:A. B(x)
T
Q
A